Nuprl Lemma : filter_wf2
0,22
postcript
pdf
T
:Type,
l
:
T
List,
P
:({
x
:
T
| (
x
l
) }
). filter(
P
;
l
)
{
x
:
T
| (
x
l
) } List
latex
Definitions
t
T
,
x
:
A
.
B
(
x
)
,
,
(
x
l
)
,
filter(
P
;
l
)
Lemmas
filter
wf
,
l
member
wf
,
bool
wf
,
list-subtype
origin
T:Type, l:T List, P:({x:T| (x 
l) }
). filter(P;l) {x:T| (x l) } List T:Type, l:T List, P:({x:T| (x l) }). filter(P;l) {x:T| (x l) } List Tx:A. B(x) l)